$\forall$$T$:Type, $L$, $L_{1}$, $L_{2}$:$T$ List.
\\[0ex]interleaving($T$;$L_{1}$;$L_{2}$;$L$)
\\[0ex]$\Leftrightarrow$
\\[0ex]($\exists$$P$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{B}$). $L_{1}$ $=$ filter2($P$;$L$) \& $L_{2}$ $=$ filter2($\lambda$$i$.$\neg_{2}$$P$($i$);$L$))